es:ES, e, e':E. (first(e))  (loc(e) = loc(e')  Id)  e loc e'  

latex

Definitions	e loc e' , t  T, P  Q, x:A. B(x), ES, E, first(e), b, loc(e), Id, , P  Q, P & Q, P  Q
Lemmas	es-le-not-locl, Id wf, es-loc wf, assert wf, es-first wf, es-E wf, event system wf, es-first-implies